Step of Proof: integer sqrt 11,40
Inference at * 1 0 1 2 1 
Iof proof for Lemma integer sqrt:



1. 0  0 
  r:. (((r * r)  0) & (0 < ((r+1) * (r+1)))) 
latex
 by ((Thin (-1)) 
CollapseTHEN (AddHiddenLabel `basecase`)) 
latex

C1: .....basecase..... NILNIL

C1: (no hyps)
C1:   r:. (((r * r)  0) & (0 < ((r+1) * (r+1))))
C.

origin